ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(x, y), 0)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(x, y), 0)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(x, y)
Used ordering: Polynomial Order [17,21] with Interpretation:
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
POL( f ) = 3
POL( 0 ) = max{0, -3}
POL( s ) = 1
POL( ap2(x1, x2) ) = max{0, 2x1 + x2 - 3}
POL( g ) = 3
POL( AP2(x1, x2) ) = max{0, 2x1 - 2}
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
AP2(ap2(ap2(g, x), y), ap2(s, z)) -> AP2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))
ap2(f, x) -> x
ap2(ap2(ap2(g, x), y), ap2(s, z)) -> ap2(ap2(ap2(g, x), y), ap2(ap2(x, y), 0))